T:Type, L1, L2, L:(T List), x:T.
no_repeats(T;L)  L1 @ [x]  L  [x / L2]  L  L1 @ [x / L2]  L 

latex

ProofTree

Definitions

t  T, L1  L2, P  Q, x:A. B(x), P & Q, P  Q, P  Q, Y, ||as||, False, A  B, i  j , x:A. B(x), A, T, ff, tt, if b then t else f fi , True, t  ...$L, , increasing(f;k), i  j < k, {i..j}, {T}, SQType(T), suptype(S; T), S  T, , i <z j, b, i z j, nth_tl(n;as), hd(l), l[i], no_repeats(T;l), Unit, , P  Q, Dec(P),

Lemmas

no repeats wf, append wf, sublist wf, length wf1, length append, int seg wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity, bnot wf, lt int wf, length nil, non neg length, length cons, le wf, assert wf, bool wf, le int wf, decidable int equal, increasing implies, select wf, not wf, select append back, select append front, increasing wf